home *** CD-ROM | disk | FTP | other *** search
/ Usenet 1993 July / InfoMagic USENET CD-ROM July 1993.ISO / answers / z-faq < prev   
Encoding:
Text File  |  1993-06-30  |  16.6 KB  |  313 lines

  1. Newsgroups: comp.specification.z,news.answers,comp.answers
  2. Path: senator-bedfellow.mit.edu!enterpoop.mit.edu!uhog.mit.edu!wupost!howland.reston.ans.net!darwin.sura.net!haven.umd.edu!uunet!pipex!uknet!comlab.ox.ac.uk!zforum-request
  3. From: zforum-request@comlab.ox.ac.uk
  4. Subject: comp.specification.z Frequently Asked Questions (Monthly)
  5. Message-ID: <z-faq_741488403@newsserv>
  6. Followup-To: comp.specification.z
  7. Summary: Information about the Z formal specification notation
  8. Originator: news@topaz.comlab
  9. Supersedes: <z-faq_738896406@newsserv>
  10. Sender: news@comlab.ox.ac.uk
  11. Reply-To: zforum-request@comlab.ox.ac.uk
  12. Organization: Oxford University Computing Laboratory, UK
  13. Date: Thu, 1 Jul 1993 01:00:11 GMT
  14. Approved: news-answers-request@MIT.Edu
  15. Expires: Thu, 12 Aug 1993 01:00:03 GMT
  16. Lines: 294
  17. Xref: senator-bedfellow.mit.edu comp.specification.z:945 news.answers:9860 comp.answers:1165
  18.  
  19. Archive-name: z-faq
  20. Last-modified: 28 June 1993
  21.  
  22.  
  23. NAME:     comp.specification.z
  24. STATUS:   unmoderated
  25. PURPOSE:  Discussion concerning the formal specification notation Z.
  26.  
  27. (If you have read this before, changed and new sections since the
  28. previously issued version are marked with `|' in the right hand margin.)
  29.  
  30. Questions have been marked with "Subject:" at the start of the line to
  31. allow some newsreaders to scan them easily (e.g., "^G" within "rn").
  32.  
  33. Subject: What is it?
  34.  
  35. The comp.specification.z USENET newsgroup was established in June 1991
  36. and is intended to handle messages concerned with the formal
  37. specification notation Z. It has an estimated readership of around
  38. 15,000 people worldwide.  Z, based on set theory and first order
  39. predicate logic, has been developed at the Programming Research Group
  40. (PRG) at the Oxford University Computing Laboratory and elsewhere for
  41. well over a decade.  It is now used by industry as part of the software
  42. (and hardware) development process in both the UK and the US. It is
  43. currently undergoing BSI standardization in the UK and has been accepted
  44. for the ISO standardisation process internationally. Comp.specification.z
  45. provides a convenient forum for messages concerned with recent
  46. developments and the use of Z.  Pointers to and reviews of recent books
  47. and articles are particularly encouraged. These will be included in the
  48. Z bibliography (see below) if they appear in comp.specification.z.
  49.  
  50. Subject: What if I know someone interested without access to USENET news?
  51.  
  52. Electronic mailing list: There is an associated Z FORUM mailing list
  53. that was initiated in January 1986 by Ruaridh Macdonald, RSRE, UK.
  54. Articles are now automatically cross-posted between comp.specification.z
  55. and the mailing list for those whose do not have access to USENET
  56. news.  This may apply especially to industrial Z users who are
  57. particularly encouraged to subscribe and post their experiences to the
  58. list.  Please contact <zforum-request@comlab.ox.ac.uk> with your name,
  59. address and e-mail address to join the mailing list (or if you change
  60. your e-mail address or wish to be removed from the list). Readers are
  61. strongly urged to read the comp.specification.z newsgroup rather than
  62. the Z FORUM mailing list if possible. Messages for submission to the Z
  63. FORUM mailing list and the comp.specification.z newsgroup may be
  64. e-mailed to <zforum@comlab.ox.ac.uk>.  This method of posting is
  65. particularly recommended for important messages like announcements of
  66. meetings since not all messages posted on \verb"comp.specification.z"
  67. reach the PRG.
  68.  
  69. Subject: What if I know someone interested without access to e-mail?
  70.  
  71. Postal mailing list: If you wish to join the postal Z mailing list,
  72. please send your address to the industrial liaison secretary at OUCL,
  73. 11 Keble Road, Oxford OX1 3QD, UK (tel +44-865-272579, fax
  74. +44-865-273839) or on <Joan.Arnold@comlab.ox.ac.uk>. This will ensure
  75. you receive details of Z meetings, etc., particularly for people
  76. without access to electronic mail.
  77.  
  78. Subject: What if I know someone interested without access to postal mail?
  79.  
  80. Be reasonable! :-)
  81.  
  82. Subject: How can I join in?
  83.  
  84. Subscribers: If you are currently using Z, you are welcome to introduce
  85. yourself to the newsgroup and Z FORUM list by describing your work with
  86. Z. You may also advertise any publications concerning Z which you or
  87. your colleagues produce. These will then be automatically added to the
  88. master Z bibliography maintained at the PRG and updated for the annual
  89. Z User Meetings held each December.
  90.  
  91. Subject: Where are the back issues and other public Z-related files?
  92.  
  93. Archive: There is an automatic mail-based electronic archive server at
  94. the PRG which contains all the back-issues and messages on Z FORUM and
  95. comp.specification.z, as well as a selection of other Z-related files.
  96. Send an e-mail message containing the command "help" to the address
  97. <archive-server@comlab.ox.ac.uk> for further information on how to use
  98. the server. A command of "index z" will list the Z-related files.
  99. If you have serious trouble accessing the archive server, please
  100. contact the address <archive-management@comlab.ox.ac.uk>.
  101.  
  102. FTP access: The archive is also available via anonymous FTP on the
  103. Internet. Type the command "ftp ftp.comlab.ox.ac.uk" (or alternatively
  104. "ftp 192.76.25.2" if this does not work) and use "anonymous" as the
  105. login id and your e-mail address as the password when prompted. The FTP
  106. command "cd Zforum" will get you into the Z archive directory.  The
  107. file "README" gives some general information and "00index" gives a list
  108. of the files. (Retrieve these using the FTP command "get README", for
  109. example.)
  110.  
  111. Subject: What tools are available?
  112.  
  113. Tools: various tools for formatting, type-checking and aiding proofs
  114. in Z are available.  A free LaTeX style file and documentation can be
  115. obtained from the PRG archive server. To receive this via e-mail, send
  116. a message containing the command "send z zed.sty zguide.tex" to the PRG
  117. archive server (see above).
  118.   The fuzz package, a syntax and type checker with a LaTeX style
  119. option and fonts, is available from J. M. Spivey Computing Science
  120. Consultancy, 34, Westlands Grove, Stockton Lane, York YO2 0EF. It is
  121. compatible with the second edition of Spivey's Z Reference Manual (see
  122. below). Contact Mike Spivey <mike@comlab.oxford.ac.uk> for further
  123. information, or send the command "send z fuzz" to the PRG
  124. archive server for an order form.
  125.   CADiZ, a suite of tools for checking and typesetting Z specifications
  126. is available from York Software Engineering, University of York, YORK
  127. YO1 5DD, UK (tel +44-904-433741, fax +44-904-433744). Support is
  128. available for Unix troff and more recently for LaTeX. Contact David
  129. Jordan at York on <yse@minster.york.ac.uk> for further information.
  130.   ProofPower is a suite of tools supporting specification and proof in
  131. Higher-Order Logic (HOL) and in Z. Short courses on ProofPower-Z are
  132. available as demand arises. For further information, contact R.B. Jones,
  133. International Computers Ltd, Eskdale Road, Winnersh, Wokingham, BERKS
  134. RG11 5TT, UK (tel +44-734-693131 ext 6536, fax +44-734-697636, email
  135. <R.B.Jones@win0109.wins.icl.co.uk>).
  136.   Zola is a tool that supports the production and typesetting of Z
  137. specifications, including a type-checker and a Tactical Proof System. The
  138. tool is sold commercially and available to academic users at a special
  139. discount.  For further information, contact K. Ashoo, Imperial
  140. Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel
  141. +44-223-462400, fax +44-223-462500, email <ka@ist.co.uk>).
  142.   The B-Tool can be used to check proofs concerning parts of Z
  143. specifications.  This is licensed by Edinburgh Portable Compilers Ltd,
  144. 17 Alva Street, Edinburgh EH2 4PH, UK (tel +44-31-225-6262, fax
  145. +44-31-225-6644). Contact the Distribution Manager on the address
  146. <support@epc.ed.ac.uk> for further information.  A Z proof tool called
  147. zedB, which is based on the B-Tool, was presented at the 1991 Z User
  148. Meeting; this may be made available in due course.
  149.   There is a Z tool for PCs which is available from Logica Cambridge.
  150. Contact Roy Maclean, Logica Cambridge Ltd, Betjeman House, 104 Hills
  151. Road, Cambridge CB2 1LQ, UK.
  152.   A survey of Z tools may be obtained from Colin Parker, Systems Process
  153. Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston
  154. PR4 1AX, UK.
  155.  
  156. Subject: How can I learn about Z?
  157.  
  158. Courses: There are a number of courses on Z run by industry and
  159. academia. Oxford University offers industrial short courses in the use
  160. Z.  As well as introductory courses, recent newly developed material
  161. includes advanced Z-based courses on proof and refinement, partly based
  162. around the zedB tool.  Courses are held in Oxford, or elsewhere (e.g.,
  163. on a company's premises) if there is enough demand. For further
  164. information, contact Jim Woodcock (tel +44-865-272576, fax
  165. +44-865-273839) on <Jim.Woodcock@comlab.ox.ac.uk>.
  166.   Logica Cambridge offer a five day course on Z and a three day
  167. introductory course on formal methods (mainly Z).  For dates and prices
  168. contact Debi Kearney on +44-223-66343 ext 4859.
  169.   Praxis Systems runs a range of Z (and other formal methods) courses.
  170. For details contact Anthony Hall on +44-225-444700 or <jah@praxis.co.uk>.
  171.  
  172. Subject: What has been published about Z?
  173.  
  174. Publications: A BibTeX bibliography of Z-related publications is
  175. available from the PRG archive server (see above).  Information on
  176. Oxford University Programming Research Group (PRG) Technical Monographs
  177. and Reports, including many on Z, is available from the librarian on
  178. <library@comlab.ox.ac.uk>.
  179.   "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993
  180. includes information on the use and teaching of Z in industry and
  181. academia.  Contact DITC Office, Formal Methods Survey, National
  182. Laboratory, Teddington, Middlesex TW11 0LW, UK (tel +44-81-943-7002,
  183. fax +44-81-977-7091) for a copy.
  184.   The following books largely concerning Z have been or are due to be
  185. published (in approximate chronological order):
  186.  
  187.   I.Hayes (ed.), Specification case studies, Prentice Hall International
  188.       Series in Computer Science, 1987.
  189.   J.M.Spivey, Understanding Z: a specification language and its formal
  190.       semantics, Cambridge University Press, 1988.
  191.   D.Ince, An introduction to discrete mathematics and formal system
  192.       specification, Oxford University Press, 1988.
  193.   J.C.P.Woodcock & M.Loomes, Software engineering mathematics, Pitman, 1988.
  194.   A.Diller, Z: an introduction to formal methods, Wiley, 1990.
  195.   J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag,
  196.       Workshops in Computing, 1990.
  197.   B.Potter, J.Sinclair & D.Till, An introduction to formal specification
  198.       and Z, Prentice Hall International Series in Computer Science, 1991.
  199.   D.Lightfoot, Formal specification using Z, MacMillan, 1991.
  200.   A.Norcliffe & G.Slater, Mathematics for software construction,
  201.       Ellis Horwood, 1991.
  202.   J.E.Nicholls (ed.), Z user workshop, Oxford 1990, Springer-Verlag,
  203.       Workshops in Computing, 1991.
  204.   I.Craig, The formal specification of advanced AI architectures,
  205.       Ellis Horwood, September 1991.
  206.   M.Imperato, An introduction to Z, Chartwell-Bratt, 1991.
  207.   J.M.Spivey, The Z notation: a reference manual, 2nd ed., Prentice Hall
  208.       International Series in Computer Science, 1992. (1st ed., 1989) +
  209.   J.B.Wordsworth, Software development with Z, Addison-Wesley, 1992.
  210.   S.Stepney, R.Barden & D.Cooper (eds.), Object orientation in Z,
  211.       Springer-Verlag, Workshops in Computing, August 1992.
  212.   J.E.Nicholls (ed.), Z user workshop, York 1991, Springer-Verlag,
  213.       Workshops in Computing, 1992.
  214.   I.Hayes (ed.), Specification case studies, 2nd ed., Prentice Hall
  215.       International Series in Computer Science, 1993.
  216.   J.P.Bowen & J.E.Nicholls (eds.), Z user workshop, London 1992,              |
  217.       Springer-Verlag, Workshops in Computing, 1993.                          |
  218.   S.Stepney, High integrity compilation: A case study, Prentice Hall, 1993.   |
  219. Announced:
  220.   K.C.Lano & H.Haughton (eds.), Object-oriented specification case studies,
  221.       Prentice Hall International Object-Oriented Series, 1993. (In press)
  222.   J.C.P.Woodcock, Using standard Z, Prentice Hall International Series
  223.       in Computer Science, 1993? (In preparation)
  224.   A.Diller, Z: an introduction to formal methods, 2nd ed., Wiley, c1994.      |
  225.       (Planned)                                                               |
  226.  
  227.   + Widely considered as the current de facto standard for Z.
  228.  
  229. Subject: What is object-oriented Z?
  230.  
  231. Several object-oriented extensions to or versions of Z have been
  232. proposed.  The book "Object orientation in Z", listed above, is a
  233. collection of papers describing various OOZ approaches -- Hall, ZERO,
  234. MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM
  235. method) -- in the main written by the methods' inventors, and all
  236. specifying the same two examples. "Object-oriented specification case
  237. studies", also listed above, surveys the principal methods and
  238. languages for formal object-oriented specification, including Z-based
  239. approaches.
  240.  
  241. Subject: How can I run Z?!
  242.  
  243. Z is a (non-executable in general) specification language, so there is
  244. no such thing as a Z compiler/linker/etc. as you would expect for a
  245. programming language. Some people have looked at animating subsets of Z
  246. for rapid prototyping purposes, using logic and functional programming
  247. for example, but this work is preliminary and is not really the major
  248. point of Z, which is to increase human understandability of the
  249. specified system and allow the possibility of formal reasoning and
  250. development. However, Prolog seems to be the main favoured language for
  251. Z prototyping and some references may be found in the Z bibliography
  252. (see above).
  253.  
  254. Subject: Where can I meet other `Z' people?
  255.  
  256. Meetings: The 7th annual Z User Meeting with an industrial theme was
  257. held on 14-15 December 1992 at the DTI A preprint proceedings and draft
  258. Z standard were distributed to delegates. A published proceedings is in
  259. press; ordering details are available from the Z archive (see above) in
  260. the file "zum92". An 8th meeting (ZUM'94) is planned for 29-30 June 1994
  261. at St. John's College, University of Cambridge, UK in association with
  262. BCS FACS. A Call for Papers has been issued and is available in the Z
  263. archive (see above) in the file "cfp94".
  264.   The 6th International Conference on Formal Description Techniques
  265. will be held at Boston, Massachusetts, USA on 26-29 October 1993.
  266. FORTE'93 will address formal techniques and testing methodologies
  267. applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1,
  268. Z, etc. For further information, contact Richard L. Tenney (Chair),
  269. Math & Computer Science, University of Massachusetts, Boston, MA
  270. 02125-3393, USA (email <rlt@cs.umb.edu>).
  271.   The 5th Refinement Workshop was held on 8-10 January 1992, at Lloyd's
  272. Register of Shipping, Fenchurch Street, London, England. The proceedings
  273. should also be published in the Springer-Verlag Workshops in Computing
  274. series. The next workshop is planned for January 1994. Please contact
  275. Roger Shaw on <ttercs@aie.lreg.co.uk> (tel +44-81-681-4747, fax
  276. +44-81-681-6814) for further information.
  277.   The first FME (Formal Methods Europe) Symposium was be held at
  278. Odense, Denmark, 19-23 April 1993.  The proceedings are available as
  279. Springer LNCS 670. The next FME Symposium will be held during September
  280. 1994 in Barcelona, Spain.  The chairman of FME is Martyn Thomas, Praxis
  281. plc, 20 Manvers Street, Bath BA1 1PX, UK (tel +44-225-444700, email
  282. <mct@praxis.co.uk>).
  283.   Details of Z-related meetings may be advertised on comp.specification.z
  284. if desired. All the above meetings are likely to be repeated in some form.
  285.  
  286. Subject: What is the Z User Group?
  287.  
  288. The Z User Group was set up in 1992 to oversee Z-related activities, and
  289. the Z User Meetings in particular.  As a subscriber to comp.specification.z,
  290. ZFORUM or the postal mailing list, you may consider yourself a member
  291. of the Z User Group.  There are currently no charges for membership,
  292. although this is subject to review if necessary.  Contact
  293. <zforum-request@comlab.ox.ac.uk> for further information.
  294.  
  295. Subject: How can I obtain the Z standard?                                     |
  296.                                                                               |
  297. The proposed Z standard is available electronically via FTP *only* (not       |
  298. via the mail server since it is too large) from the Z archive at Oxford       |
  299. in PostScript format. Version 1.0 of the draft standard is accessible as      |
  300. "zstandard1.0.ps". It is also available in printed form from the Oxford       |
  301. University Computing Laboratory librarian on <library@comlab.ox.ac.uk>        |
  302. as a Technical Monograph.                                                     |
  303.  
  304. Subject: What if I've spotted a mistake or omission?
  305.  
  306. Updates: Please send corrections or new relevant information about
  307. meetings, books, tools, etc., to <zforum-request@comlab.ox.ac.uk>.
  308. New questions and model answers are also gratefully received!
  309.  
  310. --
  311. Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk>
  312. Programming Research Group, Oxford University Computing Laboratory, UK.
  313.